/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

#pragma once
typedef enum api_object {
    seL4_UntypedObject,         /*Z 未分配内存 */
    seL4_TCBObject,             /*Z TCB */
    seL4_EndpointObject,        /*Z EP对象 */
    seL4_NotificationObject,    /*Z NF对象 */
    seL4_CapTableObject,        /*Z CSlot */
#ifdef CONFIG_KERNEL_MCS
    seL4_SchedContextObject,    /*Z 调度上下文 */
    seL4_ReplyObject,           /*Z reply对象 */
#endif
    seL4_NonArchObjectTypeCount,    /*Z 非架构相关的seL4内核对象类型数量 */
} seL4_ObjectType;

__attribute__((deprecated("use seL4_NotificationObject"))) static const seL4_ObjectType seL4_AsyncEndpointObject =
    seL4_NotificationObject;

typedef seL4_Word api_object_t;

